The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a__dbl(0) → 0
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0, cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0) → 01
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0, cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0) → 01
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0) → 0
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01) → 01
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
a__sel(s(s(X1652_3)), cons(Y, cons(X13613_3, X23614_3))) →⁺ a__sel(s(X1652_3), cons(X13613_3, X23614_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [X1652_3 / s(X1652_3), X23614_3 / cons(X13613_3, X23614_3)].
The result substitution is [Y / X13613_3].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
a__sel, mark, a__dbl1, a__sel1, a__quote

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(8) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

The following defined symbols remain to be analysed:
mark, a__sel, a__dbl1, a__sel1, a__quote

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mark.

(10) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

The following defined symbols remain to be analysed:
a__sel, a__dbl1, a__sel1, a__quote

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol a__sel.

(12) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

The following defined symbols remain to be analysed:
a__dbl1, a__sel1, a__quote

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)

Induction Base:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, 0)))

Induction Step:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, +(n79116_0, 1)))) →_R^Ω(1)
s1(s1(a__dbl1(mark(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0)))))) →_R^Ω(1)
s1(s1(a__dbl1(s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(n79116_0))))) →_IH
s1(s1(*3_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(14) Complex Obligation (BEST)

(15) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

The following defined symbols remain to be analysed:
a__sel1, a__sel, mark, a__quote

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol a__sel1.

(17) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

The following defined symbols remain to be analysed:
a__quote, a__sel, mark

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n1977765₀)

Induction Base:
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, 0)))

Induction Step:
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, +(n1977765_0, 1)))) →_R^Ω(1)
s1(a__quote(mark(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))))) →_R^Ω(1)
s1(a__quote(s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(n1977765_0)))) →_IH
s1(*3_0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(19) Complex Obligation (BEST)

(20) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n1977765₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

The following defined symbols remain to be analysed:
mark, a__sel, a__dbl1, a__sel1

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mark.

(22) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n1977765₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

The following defined symbols remain to be analysed:
a__sel, a__dbl1, a__sel1

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol a__sel.

(24) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n1977765₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

The following defined symbols remain to be analysed:
a__dbl1, a__sel1

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(25) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n3958080₀)

Induction Base:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, 0)))

Induction Step:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, +(n3958080_0, 1)))) →_R^Ω(1)
s1(s1(a__dbl1(mark(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0)))))) →_R^Ω(1)
s1(s1(a__dbl1(s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(n3958080_0))))) →_IH
s1(s1(*3_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(26) Complex Obligation (BEST)

(27) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n3958080₀)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n1977765₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

The following defined symbols remain to be analysed:
a__sel1

They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote

(28) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol a__sel1.

(29) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n3958080₀)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n1977765₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n3958080₀)

(31) BOUNDS(n^1, INF)

(32) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n3958080₀)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n1977765₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n3958080₀)

(34) BOUNDS(n^1, INF)

(35) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n1977765₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

No more defined symbols left to analyse.

(36) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)

(37) BOUNDS(n^1, INF)

(38) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote

Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))

No more defined symbols left to analyse.

(39) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n79116₀)

(40) BOUNDS(n^1, INF)